1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 -/
6
7 import analysis.normed_space.operator_norm linear_algebra.finite_dimensional tactic.omega
src └─────────────────────────────────┘ └───────────────────────────────┘ └──────────┘
8
9 /-!
10 # Finite dimensional normed spaces over complete fields
11
12 Over a complete nondiscrete field, in finite dimension, all norms are equivalent and all linear maps
13 are continuous. Moreover, a finite-dimensional subspace is always complete and closed.
14
15 ## Main results:
16
17 * `linear_map.continuous_of_finite_dimensional` : a linear map on a finite-dimensional space over a
18 complete field is continuous.
19 * `finite_dimensional.complete` : a finite-dimensional space over a complete field is complete. This
20 is not registered as an instance, as the field would be an unknown metavariable in typeclass
21 resolution.
22 * `submodule.closed_of_finite_dimensional` : a finite-dimensional subspace over a complete field is
23 closed
24 * `finite_dimensional.proper` : a finite-dimensional space over a proper field is proper. This
25 is not registered as an instance, as the field would be an unknown metavariable in typeclass
26 resolution. It is however registered as an instance for `𝕜 = ℝ` and `𝕜 = ℂ`. As properness
27 implies completeness, there is no need to also register `finite_dimensional.complete` on `ℝ` or
28 `ℂ`.
29
30 ## Implementation notes
31
32 The fact that all norms are equivalent is not written explicitly, as it would mean having two norms
33 on a single space, which is not the way type classes work. However, if one has a
34 finite-dimensional vector space `E` with a norm, and a copy `E'` of this type with another norm,
35 then the identities from `E` to `E'` and from `E'`to `E` are continuous thanks to
36 `linear_map.continuous_of_finite_dimensional`. This gives the desired norm equivalence.
37 -/
38
39 universes u v w x
40
41 open set finite_dimensional
42 open_locale classical
43
44 -- To get a reasonable compile time for `continuous_equiv_fun_basis`, typeclass inference needs
45 -- to be guided.
46 local attribute [instance, priority 10000] pi.module normed_space.to_module
id └───────┘ └────────────────────┘
src └───────┘ └────────────────────┘
typ └───────┘ └────────────────────┘
47 submodule.add_comm_group submodule.module
id └──────────────────────┘ └──────────────┘
src └──────────────────────┘ └──────────────┘
typ └──────────────────────┘ └──────────────┘
48 linear_map.finite_dimensional_range Pi.complete nondiscrete_normed_field.to_normed_field
id └─────────────────────────────────┘ └─────────┘ └──────────────────────────────────────┘
src └─────────────────────────────────┘ └─────────┘ └──────────────────────────────────────┘
typ └─────────────────────────────────┘ └─────────┘ └──────────────────────────────────────┘
doc └─────────────────────────────────┘
49
50 set_option class.instance_max_depth 100
doc └──────────────────────┘
51
52 /-- A linear map on `ι → 𝕜` (where `ι` is a fintype) is continuous -/
53 lemma linear_map.continuous_on_pi {ι : Type w} [fintype ι] {𝕜 : Type u} [normed_field 𝕜]
id └─────┘ ┴ └──────────┘ ┴
src └─────┘ └──────────┘
typ └─────┘ ┴ └──────────┘ ┴
doc └─────┘ └──────────┘
54 {E : Type v} [add_comm_group E] [vector_space 𝕜 E] [topological_space E]
id └────────────┘ ┴ └──────────┘ ┴ ┴ └───────────────┘ ┴
src └────────────┘ └──────────┘ └───────────────┘
typ └────────────┘ ┴ └──────────┘ ┴ ┴ └───────────────┘ ┴
doc └──────────┘ └───────────────┘
55 [topological_add_group E] [topological_vector_space 𝕜 E] (f : (ι → 𝕜) →ₗ[𝕜] E) : continuous f :=
id └───────────────────┘ ┴ └──────────────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ └────────┘ ┴
src └───────────────────┘ └──────────────────────┘ └─┘ ┴ └────────┘
typ └───────────────────┘ ┴ └──────────────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘┴┴ ┴ └────────┘ ┴
doc └───────────────────┘ └──────────────────────┘ └────────┘
56 begin
st └─────
57 -- for the proof, write `f` in the standard basis, and use that each coordinate is a continuous
st ──────────────────────────────────────────────────────────────────────────────────────────────────
58 -- function.
st ───────────────
59 have : (f : (ι → 𝕜) → E) =
id ┴ ┴ ┴
src └─────┘ └─┘ ┴ ┴ └┘ ┴ └┘┴└
typ └─────┘ └─┘ ┴ ┴┴└┘ ┴┴└┘┴└
doc └─────┘ └─┘ ┴ ┴ └┘ ┴ └┘ └
txt └─────┘ └─┘ ┴ ┴ └┘ ┴ └┘ └
par └─────┘ └─┘ ┴ ┴ └┘ ┴ └┘ └
pid └───┘└┘ └─┘ ┴ ┴ └┘ ┴ └┘ └
st ─────────────────────────────
60 (λx, finset.sum finset.univ (λi:ι, x i • (f (λj, if i = j then 1 else 0)))),
id └────────┘ └─────────┘ ┴ ┴ ┴
src ────────┘ └─┘└────────┘┴└─────────┘┴ └┘ └┘ ┴ ┴┴┴ ┴ └─┘ └─┘ ┴ └────────────────┘
typ ────────┘ └─┘└────────┘┴└─────────┘┴ └┘┴└┘ ┴ ┴┴┴ ┴┴ └─┘ └─┘ ┴ └────────────────┘
doc ────────┘ └─┘ ┴└─────────┘┴ └┘ └┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ └────────────────┘
txt ────────┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ └────────────────┘
par ────────┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ └────────────────┘
pid ────────┘ └─┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ └────────────────┘
st ───────────────────────────────────────────────────────────────────────────────────┘
61 by { ext x, exact f.pi_apply_eq_sum_univ x },
id └────────────────────┘ ┴
src └───┘ └────┘└────────────────────┘┴ ┴
typ └───┘ └────┘└────────────────────┘┴┴┴
doc └───┘ └────┘└────────────────────┘┴ ┴
txt └───┘ └────┘ ┴ ┴
par └───┘ └────┘ ┴ ┴
pid └┘ ┴ ┴ ┴
st ┴└────┘└───────────────────────────────┘└┘└
62 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ────────┘└─
63 refine continuous_finset_sum _ (λi hi, _),
id └───────────────────┘
src └─────┘└───────────────────┘└─┘ └──────┘
typ └─────┘└───────────────────┘└─┘ └──────┘
doc └─────┘ └─┘ └──────┘
txt └─────┘ └─┘ └──────┘
par └─────┘ └─┘ └──────┘
pid ┴ └─┘ └──────┘
st ──────────────────────────────────────────┘└─
64 exact (continuous_apply i).smul continuous_const
id └──────────────┘ ┴ └──────────────┘
src └────┘ └──────────────┘┴ └─────┘└──────────────┘┴
typ └────┘ └──────────────┘┴┴└─────┘└──────────────┘┴
doc └────┘ ┴ └─────┘ ┴
txt └────┘ ┴ └─────┘ ┴
par └────┘ ┴ └─────┘ ┴
pid ┴ ┴ └─────┘ ┴
st ──────────────────────────────────────────────────┘
65 end
st └─┘
66
67 section complete_field
68
69 variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
70 {E : Type v} [normed_group E] [normed_space 𝕜 E]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
71 {F : Type w} [normed_group F] [normed_space 𝕜 F]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
72 {F' : Type x} [add_comm_group F'] [vector_space 𝕜 F'] [topological_space F']
id └────────────┘ └──────────┘ └───────────────┘
src └────────────┘ └──────────┘ └───────────────┘
typ └────────────┘ └──────────┘ └───────────────┘
doc └──────────┘ └───────────────┘
73 [topological_add_group F'] [topological_vector_space 𝕜 F']
id └───────────────────┘ └──────────────────────┘
src └───────────────────┘ └──────────────────────┘
typ └───────────────────┘ └──────────────────────┘
doc └───────────────────┘ └──────────────────────┘
74 [complete_space 𝕜]
id └────────────┘
src └────────────┘
typ └────────────┘
doc └────────────┘
75
76 set_option class.instance_max_depth 150
doc └──────────────────────┘
77
78 /-- In finite dimension over a complete field, the canonical identification (in terms of a basis)
79 with `𝕜^n` together with its sup norm is continuous. This is the nontrivial part in the fact that
80 all norms are equivalent in finite dimension.
81 Do not use this statement as its formulation is awkward (in terms of the dimension `n`, as the proof
82 is done by induction over `n`) and it is superceded by the fact that every linear map on a
83 finite-dimensional space is continuous, in `linear_map.continuous_of_finite_dimensional`. -/
84 lemma continuous_equiv_fun_basis {n : ℕ} {ι : Type v} [fintype ι] (ξ : ι → E)
id ┴ └─────┘ ┴ ┴ ┴
src ┴ └─────┘
typ ┴ └─────┘ ┴ ┴ ┴
doc └─────┘
85 (hn : fintype.card ι = n) (hξ : is_basis 𝕜 ξ) : continuous (equiv_fun_basis hξ) :=
id └──────────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └────────┘ └─────────────┘ └┘
src └──────────┘ ┴ └──────┘ └────────┘ └─────────────┘
typ └──────────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ └────────┘ └─────────────┘ └┘
doc └──────────┘ └──────┘ └────────┘ └─────────────┘
86 begin
87 unfreezeI,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
88 induction n with n IH generalizing ι E,
src └────────┘ └─────────────────────────┘
typ └────────┘ └─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└───────┘└───────────────┘
89 { apply linear_map.continuous_of_bound _ 0 (λx, _),
src └────┘ └───┘ └───┘
typ └────┘ └───┘ └───┘
doc └────┘ └───┘ └───┘
txt └────┘ └───┘ └───┘
par └────┘ └───┘ └───┘
pid ┴ └───┘ └───┘
90 have : equiv_fun_basis hξ x = 0,
src └─────┘ ┴ ┴ ┴ └┘
typ └─────┘ ┴ ┴ ┴ └┘
doc └─────┘ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴┴
91 by { ext i, exact (fintype.card_eq_zero_iff.1 hn i).elim },
id └──────────────────────┘ └┘ ┴
src └───┘ └────┘ └──────────────────────┘└─┘ ┴ └─────┘
typ └───┘ └────┘ └──────────────────────┘└─┘└┘┴┴└─────┘
doc └───┘ └────┘ └─┘ ┴ └─────┘
txt └───┘ └────┘ └─┘ ┴ └─────┘
par └───┘ └────┘ └─┘ ┴ └─────┘
pid └┘ ┴ └─┘ ┴ └───┘└┘
st └───────────────────────────────────────┘└┘└
92 change ∥equiv_fun_basis hξ x∥ ≤ 0 * ∥x∥,
id ┴└─────────────┘ └┘ ┴ ┴ ┴ ┴
src └─────┘┴└─────────────┘┴ ┴ ┴┴┴└─┘┴┴
typ └─────┘┴└─────────────┘┴└┘┴ ┴┴┴└─┘┴┴ ┴
doc └─────┘ └─────────────┘┴ ┴ ┴ └─┘ ┴
txt └─────┘ ┴ ┴ ┴ └─┘ ┴
par └─────┘ ┴ ┴ ┴ └─┘ ┴
pid ┴ ┴ ┴ ┴ └─┘ ┴
st ──────────────────────────────────────────┘└─
93 rw this,
id └──┘
src └─┘
typ └─┘└──┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────┘└─
94 simp [norm_nonneg] },
id └─────────┘
src └────┘└─────────┘└┘
typ └────┘└─────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ──────────────────────┘└┘└
95 { haveI : finite_dimensional 𝕜 E := of_finite_basis hξ,
id └────────────────┘ ┴ ┴ └─────────────┘ └┘
src └──────┘└────────────────┘┴ ┴ └──┘└─────────────┘┴
typ └──────┘└────────────────┘┴┴┴┴└──┘└─────────────┘┴└┘
doc └──────┘└────────────────┘┴ ┴ └──┘└─────────────┘┴
txt └──────┘ ┴ ┴ └──┘ ┴
par └──────┘ ┴ ┴ └──┘ ┴
pid ┴└┘ ┴ ┴ └──┘ ┴
st ───────────────────────────────────────────────────────┘└─
96 -- first step: thanks to the inductive assumption, any n-dimensional subspace is equivalent
st ────────────────────────────────────────────────────────────────────────────────────────────────
97 -- to a standard space of dimension n, hence it is complete and therefore closed.
st ──────────────────────────────────────────────────────────────────────────────────────
98 have H₁ : ∀s : submodule 𝕜 E, findim 𝕜 s = n → is_closed (s : set E),
id └───────┘ └────┘ ┴ ┴ ┴ └───────┘ └─┘ ┴
src └────────┘ └──┘└───────┘┴ ┴ ┴└────┘┴ ┴ ┴ ┴ ┴ ┴└───────┘┴ └─┘└─┘┴ ┴
typ └────────┘ └──┘└───────┘┴ ┴ ┴└────┘┴┴┴ ┴┴┴┴┴ ┴└───────┘┴ └─┘└─┘┴┴┴
doc └────────┘ └──┘└───────┘┴ ┴ ┴└────┘┴ ┴ ┴ ┴ ┴ ┴└───────┘┴ └─┘ ┴ ┴
txt └────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
par └────────┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
pid └─────┘└─┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
99 { assume s s_dim,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ─────┘└────────────┘└─
100 rcases exists_is_basis_finite 𝕜 s with ⟨b, b_basis, b_finite⟩,
id └────────────────────┘ ┴ ┴
src └─────┘└────────────────────┘┴ ┴ └──────────────────────────┘
typ └─────┘└────────────────────┘┴┴┴┴└──────────────────────────┘
doc └─────┘ ┴ ┴ └──────────────────────────┘
txt └─────┘ ┴ ┴ └──────────────────────────┘
par └─────┘ ┴ ┴ └──────────────────────────┘
pid ┴ ┴ ┴ └──────────────────────────┘
st ──────────────────────────────────────────────────────────────────┘└─
101 letI : fintype b := finite.fintype b_finite,
id └─────┘ ┴ └────────────┘ └──────┘
src └─────┘└─────┘┴ └──┘└────────────┘┴
typ └─────┘└─────┘┴┴└──┘└────────────┘┴└──────┘
doc └─────┘└─────┘┴ └──┘└────────────┘┴
txt └─────┘ ┴ └──┘ ┴
par └─────┘ ┴ └──┘ ┴
pid ┴└┘ ┴ └──┘ ┴
st ────────────────────────────────────────────────┘└─
102 have U : uniform_embedding (equiv_fun_basis b_basis).symm,
id └───────────────┘ └─────────────┘ └─────┘
src └───────┘└───────────────┘┴ └─────────────┘┴ └────┘
typ └───────┘└───────────────┘┴ └─────────────┘┴└─────┘└────┘
doc └───────┘ ┴ └─────────────┘┴ └────┘
txt └───────┘ ┴ ┴ └────┘
par └───────┘ ┴ ┴ └────┘
pid └────┘└─┘ ┴ ┴ └───┘┴
st ──────────────────────────────────────────────────────────────┘└─
103 { have : fintype.card b = n,
id └──────────┘ ┴ ┴
src └─────┘└──────────┘┴ ┴ ┴
typ └─────┘└──────────┘┴┴┴ ┴┴
doc └─────┘└──────────┘┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴
st ───────┘└───────────────────────┘
104 by { rw ← s_dim, exact (findim_eq_card_basis b_basis).symm },
id └───┘ └──────────────────┘ └─────┘
src └───┘ └────┘ └──────────────────┘┴ └─────┘
typ └───┘└───┘ └────┘ └──────────────────┘┴└─────┘└─────┘
doc └───┘ └────┘ └──────────────────┘┴ └─────┘
txt └───┘ └────┘ ┴ └─────┘
par └───┘ └────┘ ┴ └─────┘
pid └─┘ ┴ ┴ └───┘└┘
st ┴└─────────┘└──────────────────────────────────────────┘└┘└
105 have : continuous (equiv_fun_basis b_basis) := IH (subtype.val : b → s) this b_basis,
id └────────┘ └─────────────┘ └─────┘ └┘ └─────────┘ ┴ ┴ └──┘ └─────┘
src └─────┘└────────┘┴ └─────────────┘┴ └───┘ ┴ └─────────┘└─┘ ┴ ┴ └┘ ┴
typ └─────┘└────────┘┴ └─────────────┘┴└─────┘└───┘└┘┴ └─────────┘└─┘┴┴ ┴┴└┘└──┘┴└─────┘
doc └─────┘└────────┘┴ └─────────────┘┴ └───┘ ┴ └─┘ ┴ ┴ └┘ ┴
txt └─────┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ └┘ ┴
par └─────┘ ┴ ┴ └───┘ ┴ └─┘ ┴ ┴ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴└──┘ ┴ └─┘ ┴ ┴ └┘ ┴
st ──────────────┘└────────┘└─────────────────────────────────────────────────────────────────┘└─
106 exact (equiv_fun_basis b_basis).symm.uniform_embedding (linear_map.continuous_on_pi _) this },
id └─────────────┘ └─────┘ └─────────────────────────┘ └──┘
src └────┘ └─────────────┘┴ └───────────────────────┘ └─────────────────────────┘└──┘ ┴
typ └────┘ └─────────────┘┴└─────┘└───────────────────────┘ └─────────────────────────┘└──┘└──┘┴
doc └────┘ └─────────────┘┴ └───────────────────────┘ └─────────────────────────┘└──┘ ┴
txt └────┘ ┴ └───────────────────────┘ └──┘ ┴
par └────┘ ┴ └───────────────────────┘ └──┘ ┴
pid ┴ ┴ └───────────────────────┘ └──┘ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────────────┘└┘└
107 have : is_complete (range ((equiv_fun_basis b_basis).symm)),
id └─────────┘ └───┘ └─────────────┘ └─────┘
src └─────┘└─────────┘┴ └───┘┴ └─────────────┘┴ └──────┘
typ └─────┘└─────────┘┴ └───┘┴ └─────────────┘┴└─────┘└──────┘
doc └─────┘└─────────┘┴ └───┘┴ └─────────────┘┴ └──────┘
txt └─────┘ ┴ ┴ ┴ └──────┘
par └─────┘ ┴ ┴ ┴ └──────┘
pid └───┘└┘ ┴ ┴ ┴ └──────┘
st ────────────────────────────────────────────────────────────────┘└─
108 { rw [← image_univ, is_complete_image_iff U],
id └────────┘ └───────────────────┘ ┴
src └────┘└────────┘└┘└───────────────────┘┴ ┴
typ └────┘└────────┘└┘└───────────────────┘┴┴┴
doc └────┘ └┘└───────────────────┘┴ ┴
txt └────┘ └┘ ┴ ┴
par └────┘ └┘ ┴ ┴
pid └──┘ └┘ ┴ ┴
st ───────┘└──────────────┘└───────────────────────┘└──
109 convert complete_univ,
id └───────────┘
src └──────┘└───────────┘
typ └──────┘└───────────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ────────────────────────────┘└─
110 change complete_space (b → 𝕜),
id └────────────┘ ┴ ┴
src └─────┘└────────────┘┴ ┴ ┴ ┴
typ └─────┘└────────────┘┴ ┴┴ ┴┴┴
doc └─────┘└────────────┘┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────┘
111 apply_instance },
st └┘
112 have : is_complete (range (subtype.val : s → E)),
id ┴
typ ┴
113 { change is_complete (range ((equiv_fun_basis b_basis).symm.to_equiv)) at this,
114 rw equiv.range_eq_univ at this,
115 rwa [← image_univ, is_complete_image_iff],
116 exact isometry_subtype_val.uniform_embedding },
st └┘
117 apply is_closed_of_is_complete,
118 rwa subtype.val_range at this },
st └┘
119 -- second step: any linear form is continuous, as its kernel is closed by the first step
120 have H₂ : ∀f : E →ₗ[𝕜] 𝕜, continuous f,
id ┴ ┴
typ ┴ ┴
121 { assume f,
122 have : findim 𝕜 f.ker = n ∨ findim 𝕜 f.ker = n.succ,
id ┴ └────┘
src └────┘
typ ┴ └────┘
123 { have Z := f.findim_range_add_findim_ker,
124 rw [findim_eq_card_basis hξ, hn] at Z,
125 have : findim 𝕜 f.range = 0 ∨ findim 𝕜 f.range = 1,
id ┴
typ ┴
126 { have I : ∀(k : ℕ), k ≤ 1 ↔ k = 0 ∨ k = 1, by omega manual,
127 have : findim 𝕜 f.range ≤ findim 𝕜 𝕜 := submodule.findim_le _,
id ┴
typ ┴
128 rwa [findim_of_field, I] at this },
st └┘
129 cases this,
130 { rw this at Z,
131 right,
132 simpa using Z },
st └┘
133 { left,
134 rw [this, add_comm, nat.add_one] at Z,
135 exact nat.succ_inj Z } },
st └──┘
136 have : is_closed (f.ker : set E),
id └─┘ ┴
src └─┘
typ └─┘ ┴
137 { cases this,
138 { exact H₁ _ this },
st └┘
139 { have : f.ker = ⊤,
140 by { apply eq_top_of_findim_eq, rw [findim_eq_card_basis hξ, hn, this] },
st ┴ └┘
141 simp [this] } },
st └──┘
142 exact linear_map.continuous_iff_is_closed_ker.2 this },
st └┘
143 -- third step: applying the continuity to the linear form corresponding to a coefficient in the
144 -- basis decomposition, deduce that all such coefficients are controlled in terms of the norm
145 have : ∀i:ι, ∃C, 0 ≤ C ∧ ∀(x:E), ∥equiv_fun_basis hξ x i∥ ≤ C * ∥x∥,
id ┴ ┴ ┴
typ ┴ ┴ ┴
146 { assume i,
147 let f : E →ₗ[𝕜] 𝕜 := (linear_map.proj i).comp (equiv_fun_basis hξ),
id ┴ ┴ ┴
typ ┴ ┴ ┴
148 let f' : E →L[𝕜] 𝕜 := { cont := H₂ f, ..f },
id ┴ ┴
typ ┴ ┴
149 exact ⟨∥f'∥, norm_nonneg _, λx, continuous_linear_map.le_op_norm f' x⟩ },
id ┴
typ ┴
st └┘
150 -- fourth step: combine the bound on each coefficient to get a global bound and the continuity
151 choose C0 hC0 using this,
152 let C := finset.sum finset.univ C0,
id └┘
typ └┘
153 have C_nonneg : 0 ≤ C := finset.sum_nonneg (λi hi, (hC0 i).1),
id ┴ ┴
typ ┴ ┴
154 have C0_le : ∀i, C0 i ≤ C :=
id ┴ └┘ ┴
typ ┴ └┘ ┴
155 λi, finset.single_le_sum (λj hj, (hC0 j).1) (finset.mem_univ _),
id ┴ ┴
typ ┴ ┴
156 apply linear_map.continuous_of_bound _ C (λx, _),
id ┴ ┴
typ ┴ ┴
157 rw pi_norm_le_iff,
158 { exact λi, le_trans ((hC0 i).2 x) (mul_le_mul_of_nonneg_right (C0_le i) (norm_nonneg _)) },
id ┴ ┴
typ ┴ ┴
st └┘
159 { exact mul_nonneg C_nonneg (norm_nonneg _) } }
st └───
160 end
st ──┘
161
162 /-- Any linear map on a finite dimensional space over a complete field is continuous. -/
163 theorem linear_map.continuous_of_finite_dimensional [finite_dimensional 𝕜 E] (f : E →ₗ[𝕜] F') :
id ┴ ┴ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘
164 continuous f :=
165 begin
166 -- for the proof, go to a model vector space `b → 𝕜` thanks to `continuous_equiv_fun_basis`, and
167 -- argue that all linear maps there are continuous.
168 rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
id ┴ ┴
typ ┴ ┴
169 letI : fintype b := finite.fintype b_finite,
id └─────┘ ┴ └──────┘
src └─────┘
typ └─────┘ ┴ └──────┘
doc └─────┘
170 have A : continuous (equiv_fun_basis b_basis) :=
171 continuous_equiv_fun_basis _ rfl b_basis,
172 have B : continuous (f.comp ((equiv_fun_basis b_basis).symm : (b → 𝕜) →ₗ[𝕜] E)) :=
id ┴ ┴
typ ┴ ┴
173 linear_map.continuous_on_pi _,
174 have : continuous ((f.comp ((equiv_fun_basis b_basis).symm : (b → 𝕜) →ₗ[𝕜] E))
id ┴ ┴
typ ┴ ┴
175 ∘ (equiv_fun_basis b_basis)) := B.comp A,
176 convert this,
177 ext x,
178 simp only [linear_equiv.coe_apply, function.comp_app, coe_fn_coe_base, linear_map.comp_apply],
179 rw linear_equiv.symm_apply_apply
180 end
st └─┘
181
182 /-- The continuous linear map induced by a linear map on a finite dimensional space -/
183 def linear_map.to_continuous_linear_map [finite_dimensional 𝕜 E] (f : E →ₗ[𝕜] F') : E →L[𝕜] F' :=
id ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
typ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └┘
184 { cont := f.continuous_of_finite_dimensional, ..f }
185
186 /-- The continuous linear equivalence induced by a linear equivalence on a finite dimensional space. -/
187 def linear_equiv.to_continuous_linear_equiv [finite_dimensional 𝕜 E] (e : E ≃ₗ[𝕜] F) : E ≃L[𝕜] F :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
188 { continuous_to_fun := e.to_linear_map.continuous_of_finite_dimensional,
id └───────────┘└───────────────────────────────┘
src └───────────┘└───────────────────────────────┘
typ └───────────┘└───────────────────────────────┘
doc └───────────────────────────────┘
189 continuous_inv_fun := begin
st └─────
190 haveI : finite_dimensional 𝕜 F := e.finite_dimensional,
id └────────────────┘ ┴ ┴ └──────────────────┘
src └──────┘└────────────────┘┴ ┴ └──┘└──────────────────┘
typ └──────┘└────────────────┘┴┴┴┴└──┘└──────────────────┘
doc └──────┘└────────────────┘┴ ┴ └──┘└──────────────────┘
txt └──────┘ ┴ ┴ └──┘
par └──────┘ ┴ ┴ └──┘
pid ┴└┘ ┴ ┴ └──┘
st ─────────────────────────────────────────────────────────┘└─
191 exact e.symm.to_linear_map.continuous_of_finite_dimensional
id └───────────────────────────────────────────────────┘
src └────┘└───────────────────────────────────────────────────┘└
typ └────┘└───────────────────────────────────────────────────┘└
doc └────┘└───────────────────────────────────────────────────┘└
txt └────┘ └
par └────┘ └
pid ┴ └
st ────────────────────────────────────────────────────────────────
192 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
193 ..e }
id ┴
typ ┴
194
195 /-- Any finite-dimensional vector space over a complete field is complete.
196 We do not register this as an instance to avoid an instance loop when trying to prove the
197 completeness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance
198 explicitly when needed. -/
199 variables (𝕜 E)
200 lemma finite_dimensional.complete [finite_dimensional 𝕜 E] : complete_space E :=
id └────────────────┘ ┴ ┴ └────────────┘ ┴
src └────────────────┘ └────────────┘
typ └────────────────┘ ┴ ┴ └────────────┘ ┴
doc └────────────────┘ └────────────┘
201 begin
st └─────
202 rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
id └────────────────────┘ ┴ ┴
src └─────┘└────────────────────┘┴ ┴ └──────────────────────────┘
typ └─────┘└────────────────────┘┴┴┴┴└──────────────────────────┘
doc └─────┘ ┴ ┴ └──────────────────────────┘
txt └─────┘ ┴ ┴ └──────────────────────────┘
par └─────┘ ┴ ┴ └──────────────────────────┘
pid ┴ ┴ ┴ └──────────────────────────┘
st ──────────────────────────────────────────────────────────────┘└─
203 letI : fintype b := finite.fintype b_finite,
id └─────┘ ┴ └────────────┘ └──────┘
src └─────┘└─────┘┴ └──┘└────────────┘┴
typ └─────┘└─────┘┴┴└──┘└────────────┘┴└──────┘
doc └─────┘└─────┘┴ └──┘└────────────┘┴
txt └─────┘ ┴ └──┘ ┴
par └─────┘ ┴ └──┘ ┴
pid ┴└┘ ┴ └──┘ ┴
st ────────────────────────────────────────────┘└─
204 have : uniform_embedding (equiv_fun_basis b_basis).symm :=
id └───────────────┘ └─────────────┘ └─────┘
src └─────┘└───────────────┘┴ └─────────────┘┴ └─────────
typ └─────┘└───────────────┘┴ └─────────────┘┴└─────┘└─────────
doc └─────┘ ┴ └─────────────┘┴ └─────────
txt └─────┘ ┴ ┴ └─────────
par └─────┘ ┴ ┴ └─────────
pid └───┘└┘ ┴ ┴ └───┘└────
st ─────────────────────────────────────────────────────────────
205 linear_equiv.uniform_embedding _ (linear_map.continuous_of_finite_dimensional _)
id └────────────────────────────┘
src ───┘└────────────────────────────┘└─┘ └───
typ ───┘└────────────────────────────┘└─┘ └───
doc ───┘└────────────────────────────┘└─┘ └───
txt ───┘ └─┘ └───
par ───┘ └─┘ └───
pid ───┘ └─┘ └───
st ─────────────────────────────────────────────────────────────────────────────────────
206 (linear_map.continuous_of_finite_dimensional _),
id └─────────────────────────────────────────┘
src ───┘ └─────────────────────────────────────────┘└─┘
typ ───┘ └─────────────────────────────────────────┘└─┘
doc ───┘ └─────────────────────────────────────────┘└─┘
txt ───┘ └─┘
par ───┘ └─┘
pid ───┘ └─┘
st ──────────────────────────────────────────────────┘└─
207 have : is_complete ((equiv_fun_basis b_basis).symm.to_equiv '' univ) :=
id └─────────┘ └─────────────┘ └─────┘ └┘ └──┘
src └─────┘└─────────┘┴ └─────────────┘┴ └──────────────┘└┘┴└──┘└────
typ └─────┘└─────────┘┴ └─────────────┘┴└─────┘└──────────────┘└┘┴└──┘└────
doc └─────┘└─────────┘┴ └─────────────┘┴ └──────────────┘ ┴ └────
txt └─────┘ ┴ ┴ └──────────────┘ ┴ └────
par └─────┘ ┴ ┴ └──────────────┘ ┴ └────
pid └───┘└┘ ┴ ┴ └──────────────┘ ┴ ┴└───
st ──────────────────────────────────────────────────────────────────────────
208 (is_complete_image_iff this).mpr complete_univ,
id └───────────────────┘ └───────────┘
src ───┘ └───────────────────┘┴ └────┘└───────────┘
typ ───┘ └───────────────────┘┴ └────┘└───────────┘
doc ───┘ └───────────────────┘┴ └────┘
txt ───┘ ┴ └────┘
par ───┘ ┴ └────┘
pid ───┘ ┴ └────┘
st ──────────────────────────┘ └─────────────────┘
209 rw [image_univ, equiv.range_eq_univ] at this,
210 exact complete_space_of_is_complete_univ this
211 end
st └─┘
212
213 variables {𝕜 E}
214 /-- A finite-dimensional subspace is complete. -/
215 lemma submodule.complete_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
id └───────┘ ┴ ┴ └────────────────┘ ┴ ┴
src └───────┘ └────────────────┘
typ └───────┘ ┴ ┴ └────────────────┘ ┴ ┴
doc └───────┘ └────────────────┘
216 is_complete (s : set E) :=
id └─────────┘ ┴ └─┘ ┴
src └─────────┘ └─┘
typ └─────────┘ ┴ └─┘ ┴
doc └─────────┘
217 begin
st └─────
218 haveI : complete_space s := finite_dimensional.complete 𝕜 s,
id └────────────┘ ┴ └─────────────────────────┘ ┴ ┴
src └──────┘└────────────┘┴ └──┘└─────────────────────────┘┴ ┴
typ └──────┘└────────────┘┴┴└──┘└─────────────────────────┘┴┴┴┴
doc └──────┘└────────────┘┴ └──┘ ┴ ┴
txt └──────┘ ┴ └──┘ ┴ ┴
par └──────┘ ┴ └──┘ ┴ ┴
pid ┴└┘ ┴ └──┘ ┴ ┴
st ────────────────────────────────────────────────────────────┘└─
219 have : is_complete (range (subtype.val : s → E)),
id └─────────┘ └───┘ └─────────┘ ┴ ┴
src └─────┘└─────────┘┴ └───┘┴ └─────────┘└─┘ ┴ ┴ └┘
typ └─────┘└─────────┘┴ └───┘┴ └─────────┘└─┘┴┴ ┴┴└┘
doc └─────┘└─────────┘┴ └───┘┴ └─┘ ┴ ┴ └┘
txt └─────┘ ┴ ┴ └─┘ ┴ ┴ └┘
par └─────┘ ┴ ┴ └─┘ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ └─┘ ┴ ┴ └┘
st ─────────────────────────────────────────────────┘└─
220 { rw [← image_univ, is_complete_image_iff],
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid └──┘
st ───┘└──────────────┘
221 { exact complete_univ },
st ┴
222 { exact isometry_subtype_val.uniform_embedding } },
st └─┘
223 rwa subtype.val_range at this
224 end
st └─┘
225
226 /-- A finite-dimensional subspace is closed. -/
227 lemma submodule.closed_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
id └───────┘ ┴ ┴ └────────────────┘ ┴ ┴
src └───────┘ └────────────────┘
typ └───────┘ ┴ ┴ └────────────────┘ ┴ ┴
doc └───────┘ └────────────────┘
228 is_closed (s : set E) :=
id └───────┘ ┴ └─┘ ┴
src └───────┘ └─┘
typ └───────┘ ┴ └─┘ ┴
doc └───────┘
229 is_closed_of_is_complete s.complete_of_finite_dimensional
id └──────────────────────┘ ┴┴
src └──────────────────────┘ ┴
typ └──────────────────────┘ ┴┴
doc ┴
230
231 end complete_field
232
233 section proper_field
234 variables (𝕜 : Type u) [nondiscrete_normed_field 𝕜]
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
235 (E : Type v) [normed_group E] [normed_space 𝕜 E] [proper_space 𝕜]
id └──────────┘ └──────────┘ └──────────┘
src └──────────┘ └──────────┘ └──────────┘
typ └──────────┘ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘ └──────────┘
236
237 /-- Any finite-dimensional vector space over a proper field is proper.
238 We do not register this as an instance to avoid an instance loop when trying to prove the
239 properness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance
240 explicitly when needed. -/
241 lemma finite_dimensional.proper [finite_dimensional 𝕜 E] : proper_space E :=
id └────────────────┘ ┴ ┴ └──────────┘ ┴
src └────────────────┘ └──────────┘
typ └────────────────┘ ┴ ┴ └──────────┘ ┴
doc └────────────────┘ └──────────┘
242 begin
st └─────
243 rcases exists_is_basis_finite 𝕜 E with ⟨b, b_basis, b_finite⟩,
id └────────────────────┘ ┴ ┴
src └─────┘└────────────────────┘┴ ┴ └──────────────────────────┘
typ └─────┘└────────────────────┘┴┴┴┴└──────────────────────────┘
doc └─────┘ ┴ ┴ └──────────────────────────┘
txt └─────┘ ┴ ┴ └──────────────────────────┘
par └─────┘ ┴ ┴ └──────────────────────────┘
pid ┴ ┴ ┴ └──────────────────────────┘
st ──────────────────────────────────────────────────────────────┘└─
244 letI : fintype b := finite.fintype b_finite,
id └─────┘ ┴ └────────────┘ └──────┘
src └─────┘└─────┘┴ └──┘└────────────┘┴
typ └─────┘└─────┘┴┴└──┘└────────────┘┴└──────┘
doc └─────┘└─────┘┴ └──┘└────────────┘┴
txt └─────┘ ┴ └──┘ ┴
par └─────┘ ┴ └──┘ ┴
pid ┴└┘ ┴ └──┘ ┴
st ────────────────────────────────────────────┘└─
245 let e := equiv_fun_basis b_basis,
id └─────────────┘ └─────┘
src └───────┘└─────────────┘┴
typ └───────┘└─────────────┘┴└─────┘
doc └───────┘└─────────────┘┴
txt └───────┘ ┴
par └───────┘ ┴
pid └───┘┴└─┘ ┴
st ─────────────────────────────────┘
246 let f : E →L[𝕜] (b → 𝕜) :=
id ┴ ┴
typ ┴ ┴
247 { cont := linear_map.continuous_of_finite_dimensional _, ..e.to_linear_map },
248 refine metric.proper_image_of_proper e.symm
249 (linear_map.continuous_of_finite_dimensional _) _ (∥f∥) (λx y, _),
250 { exact equiv.range_eq_univ e.symm.to_equiv },
st └┘
251 { have A : e (e.symm x) = x := linear_equiv.apply_symm_apply _ _,
252 have B : e (e.symm y) = y := linear_equiv.apply_symm_apply _ _,
253 conv_lhs { rw [← A, ← B] },
254 change dist (f (e.symm x)) (f (e.symm y)) ≤ ∥f∥ * dist (e.symm x) (e.symm y),
255 exact f.lipschitz _ _ }
st └─
256 end
st ──┘
257
258 end proper_field
259
260 /- Over the real numbers, we can register the previous statement as an instance as it will not
261 cause problems in instance resolution since the properness of `ℝ` is already known. -/
262 instance finite_dimensional.proper_real
263 (E : Type u) [normed_group E] [normed_space ℝ E] [finite_dimensional ℝ E] : proper_space E :=
id └┘ └──┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └──┘ └┘ ┴ ┴
typ └┘ └──┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └──┘ └┘
264 finite_dimensional.proper ℝ E
id ┴ ┴
src ┴
typ ┴ ┴
265
266 attribute [instance, priority 900] finite_dimensional.proper_real